DS($A$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$${\it sort}$:($A$$\rightarrow$Type)$\times$($a$:$A$$\rightarrow$EqDecider(${\it sort}$($a$)))